<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue2744</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

\noindent Before.
\begin{AgdaMultiCode}
</a><a id="103" class="Markup">\begin{code}[hide]</a>
  <a id="124" class="Keyword">postulate</a>
<a id="134" class="Markup">\end{code}</a><a id="144" class="Background">
</a><a id="145" class="Markup">\begin{code}</a>
    <a id="A"></a><a id="162" href="Issue2744.html#162" class="Postulate">A</a>    <a id="167" class="Symbol">:</a> <a id="169" class="PrimitiveType">Set</a>
<a id="173" class="Markup">\end{code}</a><a id="183" class="Background">
</a><a id="184" class="Markup">\begin{code}</a>
    <a id="BBB"></a><a id="201" href="Issue2744.html#201" class="Postulate">BBB</a>  <a id="206" class="Symbol">:</a> <a id="208" class="PrimitiveType">Set</a>
<a id="212" class="Markup">\end{code}</a><a id="222" class="Background">
\end{AgdaMultiCode}
After.

\noindent Before.
\begin{AgdaAlign}
</a><a id="287" class="Markup">\begin{code}</a>
  <a id="302" class="Keyword">postulate</a>
    <a id="C"></a><a id="316" href="Issue2744.html#316" class="Postulate">C</a> <a id="318" class="Symbol">:</a> <a id="320" class="PrimitiveType">Set</a>
<a id="324" class="Markup">\end{code}</a><a id="334" class="Background">
</a><a id="335" class="Markup">\begin{code}[hide]</a>
    <a id="D"></a><a id="358" href="Issue2744.html#358" class="Postulate">D</a> <a id="360" class="Symbol">:</a> <a id="362" class="PrimitiveType">Set</a>
<a id="366" class="Markup">\end{code}</a><a id="376" class="Background">
</a><a id="377" class="Markup">\begin{code}</a>
    <a id="E"></a><a id="394" href="Issue2744.html#394" class="Postulate">E</a> <a id="396" class="Symbol">:</a> <a id="398" class="PrimitiveType">Set</a>
<a id="402" class="Markup">\end{code}</a><a id="412" class="Background">
\end{AgdaAlign}
After.

\noindent Before.
\begin{AgdaAlign}
</a><a id="473" class="Markup">\begin{code}</a>
  <a id="488" class="Keyword">postulate</a>
    <a id="F"></a><a id="502" href="Issue2744.html#502" class="Postulate">F</a> <a id="504" class="Symbol">:</a> <a id="506" class="PrimitiveType">Set</a>
<a id="510" class="Markup">\end{code}</a><a id="520" class="Background">
In between.
\begin{AgdaSuppressSpace}
</a><a id="559" class="Markup">\begin{code}</a>
  <a id="574" class="Keyword">postulate</a>
    <a id="G"></a><a id="588" href="Issue2744.html#588" class="Postulate">G</a> <a id="590" class="Symbol">:</a> <a id="592" class="PrimitiveType">Set</a>
<a id="596" class="Markup">\end{code}</a><a id="606" class="Background">
</a><a id="607" class="Markup">\begin{code}[hide]</a>
  <a id="628" class="Keyword">postulate</a>
<a id="638" class="Markup">\end{code}</a><a id="648" class="Background">
</a><a id="649" class="Markup">\begin{code}</a>
    <a id="H"></a><a id="666" href="Issue2744.html#666" class="Postulate">H</a> <a id="668" class="Symbol">:</a> <a id="670" class="PrimitiveType">Set</a>
<a id="674" class="Markup">\end{code}</a><a id="684" class="Background">
\end{AgdaSuppressSpace}
\end{AgdaAlign}
After.

\noindent Before.
\begin{AgdaMultiCode}
</a><a id="773" class="Markup">\begin{code}</a>
  <a id="788" class="Keyword">postulate</a>
    <a id="!_!"></a><a id="802" href="Issue2744.html#802" class="Postulate Operator">!_!</a>    <a id="809" class="Symbol">:</a> <a id="811" class="PrimitiveType">Set</a> <a id="815" class="Symbol">→</a> <a id="817" class="PrimitiveType">Set</a>
<a id="821" class="Markup">\end{code}</a><a id="831" class="Background">
</a><a id="832" class="Markup">\begin{code}[hide]</a>
  <a id="853" class="Keyword">postulate</a>
<a id="863" class="Markup">\end{code}</a><a id="873" class="Background">
</a><a id="874" class="Markup">\begin{code}</a>
    <a id="&lt;!_!&gt;"></a><a id="891" href="Issue2744.html#891" class="Postulate Operator">&lt;!_!&gt;</a>  <a id="898" class="Symbol">:</a> <a id="900" class="PrimitiveType">Set</a> <a id="904" class="Symbol">→</a> <a id="906" class="PrimitiveType">Set</a>
<a id="910" class="Markup">\end{code}</a><a id="920" class="Background">
\end{AgdaMultiCode}
After.

\end{document}
</a></pre></body></html>